REQ-70 file family: do not route — the gap is a security bypass - #72

Metrics unchanged in substance (3323 tests, 12678 Qed, 0 admits, 0 axioms);
timestamp, commit stamp and the rebuilt WASM asset only. The published count
is correct this round — the fail-closed guard added after the #69 chain (where
the deploy prebuild silently published 2659 for a true 3284) did its job.

dim1_dim9 promotion_ready reads true for the same container-local reason
recorded at the #68/#69 chains: the pinned tla2tools/alloy jars are on disk
here. Top-line verdict unchanged: overall_foundation FAIL.

…te fail/vfs

REQ-70. The file family was held back because routing it would have let a
compiled binary bypass a Coq-modeled access-control check that riinac run
enforces (12 gate call sites in the interpreter, 0 gating constructs in the C
helpers). The gate is now mirrored, so the family routes.

DESIGN, recorded because the obvious approach is impossible. Emitted C cannot
call into Rust: the pipeline is `cc -o out one.c` with nothing linked, so a
single shared implementation callable from both backends would mean shipping
per-target Rust staticlibs (native/wasm32/android/ios) and rebuilding the
compile pipeline. Instead the COQ MODEL is the single source of truth —
domains/VerifiedFileSystem.v (Inode/Ownership/Permission/is_owner/
get_permission) — with riina-os/src/vfs.rs and the emitted C as two
implementations of it, held together by a differential. Same shape as the masa
civil calendar and the GF128/AES Coq-Rust equivalences.

The C mirrors: the inode table, first-touch ownership at mode 0644 (owner rw,
group/other r), owner > group > other resolution, can_read/can_write as
is_root OR the applicable bit, and gate_delete clearing the mapping so a
re-creator owns the file. Denial exits non-zero with the interpreter's wording
and cannot fall through to the filesystem.

Matched op-for-op, including the negative space: fail_ada and fail_senarai are
UNGATED in the interpreter (an existence check is not an access), so they are
ungated in C too. Gating them would have been a divergence in the opposite
direction — denying what the interpreter allows.

Deliberately NOT the host OS's own permission bits: the gate is RIINA's model
and must deny where the model denies even when the host would allow (the
process typically owns these files), so letting the kernel decide would
silently make the check a no-op.

Routed: the 8 fail_* builtins plus vfs_mula/vfs_jadi_pengguna, which are what
make the gate meaningful. vfs_tulis/vfs_baca/vfs_padam stay interpreter-only —
they operate on the in-memory VirtualFs with quota accounting that has no C
implementation, and stubbing them would claim an enforcement this backend
cannot make.

THE #72 LIMITATION IS NOW CLOSED. file_gate_parity.rs's active SECURITY
REGRESSION arm was previously unexecutable — no vfs C helpers existed to build
the bypass with — and is now negative-controlled: deleting a single riina_gate
call from the emitted fail_tulis makes the compiled binary perform the write
(exit 0) and the test fails with its intended message.

Adds file_differential.rs (7 cases), chosen to separate the resolution arms
rather than to demonstrate the happy path: owner write; non-owner read ALLOWED
at 0644; non-owner write and append DENIED; delete clears ownership so a
different uid may re-create and own; ungated existence check. A C gate that
collapsed owner/group/other by always consulting perm_owner would pass a naive
same-uid test and fail these.

Also updates pkg_build's interpreter-only boundary example from fail_baca (now
compiles) to vfs_baca — a deliberate choice rather than the next arbitrary
one, since the VirtualFs quota has no C implementation and so it should stay
interpreter-only for as long as that holds. The test's own comment asks for
exactly this update.

Verified: 03_PROTO 3330/0 (+7), 05_TOOLING 323/0, clippy clean on both,
audit-docs.sh 0 discrepancies. STDLIB.md regenerated from the compiler:
fail_* and the two setters native-only, the VirtualFs trio still interp-only.

… fail/vfs

The file family was held back in #72 because routing it would have let a
compiled binary bypass a Coq-modeled access-control check that riinac run
enforces (12 gate call sites in the interpreter, 0 in the C helpers). The gate
is now mirrored, so the family routes.

Design: emitted C cannot call into Rust — the pipeline is `cc -o out one.c`
with nothing linked — so a single shared implementation would have meant
per-target Rust staticlibs. Instead the Coq model is the single source of
truth (domains/VerifiedFileSystem.v), with riina-os/src/vfs.rs and the emitted
C as two implementations of it, held together by a differential. Same shape as
the masa civil calendar and the GF128/AES Coq-Rust equivalences.

Matched op-for-op including the negative space: fail_ada and fail_senarai are
ungated in the interpreter, so they are ungated in C — gating them would be a
divergence in the opposite direction.

Routed: 8 fail_* plus vfs_mula/vfs_jadi_pengguna. The VirtualFs trio stays
interpreter-only; its quota accounting has no C implementation and stubbing it
would claim an enforcement this backend cannot make.

The #72 limitation is closed: file_gate_parity.rs's active SECURITY REGRESSION
arm was previously unexecutable and is now negative-controlled — deleting one
riina_gate call makes the compiled binary perform the forbidden write and the
test fails.

Adds file_differential.rs (7 cases) chosen to separate the owner/group/other
resolution arms rather than demonstrate the happy path.

Also records the keselamatan inspection: its taint discipline is compile-time
(verified by running riinac check), only 3 of 42 have a runtime property, and
those call the same gate — so this PR covers them too.

3330/0 tests in 03_PROTO, 323/0 in 05_TOOLING, clippy clean, 0 doc
discrepancies.